(* $Id: PFOLEncodedEnv.mli 117 2007-10-21 17:27:07Z yann.regisgianas $ *)

(* Pangolin, a functional programming language for correct programs.
   Copyright (C) 2007, Yann Régis-Gianas, François Pottier.
   Contact: yann.regisgianas@gmail.com

   This program is free software: you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   any later version.

   This program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program.  If not, see <http://www.gnu.org/licenses/>. *)

(** This module provides a twin environment that is synchronized with
    the typing environment but contains the first order logic encoding
    of its logical part. This enables the incremental encoding of the
    program hypothesis to generate proof obligations in PFOL quickly. *)

(** FIXME *)
type env = PFOLEnv.env

(** FIXME *)
val empty: env

(** FIXME *)
val introduce_rigid_type_variables : 
  Position.t -> env -> (XCoreSyntax.tid * XCoreSyntax.kind) list -> env


(** FIXME *)
val bind_value :
  Position.t ->
  PFOLEnv.env ->
  XCoreSyntax.id ->
  XCoreSyntax.type_scheme ->
  PFOLEnv.env * PFOLSyntax.value_identifier

(** FIXME *)
val bind_logic_value :
  Position.t ->
  PFOLEnv.env ->
  XCoreSyntax.id ->
  XCoreSyntax.formula_type_scheme ->
  PFOLEnv.env * PFOLSyntax.value_identifier

(** FIXME *)
val bind_fact :
  Position.position -> PFOLEnv.env -> XCoreSyntax.lformula -> PFOLEnv.env

(** FIXME *)
val bind_logic_function :
  Position.t ->
  PFOLEnv.env ->
  XCoreSyntax.id -> XCoreSyntax.formula_type_scheme -> PFOLEnv.env

(** FIXME *)
val logic_clause_as_formula :
  Position.position ->
  XCoreSyntax.var ->
  XCoreSyntax.formula_type ->
  XCoreSyntax.fbindings ->
  XCoreSyntax.opaque_logic_clause_abs -> XCoreSyntax.formula

(** FIXME *)
val bind_logic_function_definition :
  Position.position ->
  PFOLEnv.env ->
  XCoreSyntax.id ->
  XCoreSyntax.formula_type_scheme ->
  XCoreSyntax.logic_function_definition -> PFOLEnv.env

(** [bind_predicate_type_scheme pos env p s] introduces two atoms in
    PFOL.  The first one is a predicate whose type scheme is the
    encoding of [s].  The second one is an object whose type scheme is
    the object encoding of [s]. *)
val bind_predicate_type_scheme :
  Position.t ->
  PFOLEnv.env ->
  XCoreSyntax.pid -> XCoreSyntax.formula_type_scheme -> PFOLEnv.env

(** [bind_predicate_defintion] encodes a PHOL predicate definition in PFOL. 

    - Abbreviations are encoded using propositional equivalence. 
    - Inductive definitions are axiomatized. *)
val bind_predicate_definition :
  Position.position ->
  PFOLEnv.env ->
  XCoreSyntax.pid ->
  XCoreSyntax.formula_type_scheme ->
  XCoreSyntax.predicate_definition -> PFOLEnv.env

(** FIXME *)
val bind_dataconstructor :
  Position.position ->
  XCoreSyntax.type_parameters ->
  PFOLEnv.env -> 
  XCoreSyntax.id * XCoreSyntax.type_parameters * XCoreSyntax.term_type -> 
  PFOLEnv.env

(** FIXME *)
val bind_type_definition :
  Position.position ->
  PFOLEnv.env ->
  XCoreSyntax.tid ->
  XCoreSyntax.kind -> XCoreSyntax.type_definition -> PFOLEnv.env
